theory Design_Sec
imports "../../GPTEE_Function_Layer/Security/REQ_SEC"
"./Design_Sec_OpenSession"
"./Design_Sec_InvokeCommand"
"./Design_Sec_CloseSession"
"./Design_Sec_Memory"
begin
section "Design level proof"
lemma s0_ref_lemma : "(⇑s0r) = s0t"
using s0t_init s0r_init system_initR_def
by (metis (full_types) State.select_convs(1) State.select_convs(2)
State.select_convs(3) State.select_convs(4) State.select_convs(5)
State.select_convs(6) State.surjective abstract_state_def old.unit.exhaust)
lemma sysR_refine : "(s,t) ∈exec_eventR (sys' Reserved) ⟶ (⇑s,⇑t)∈exec_event ((eR (sys' Reserved)))"
using exec_eventR_def exec_event_def eR_def by auto
lemma refine_exec_event : "(s,t)∈exec_eventR e ⟹
(⇑s,⇑t)∈exec_event ((eR e))"
proof -
assume p0:"(s,t)∈exec_eventR e"
then show "(⇑s,⇑t)∈exec_event ((eR e))"
proof(induct e)
case (hyperc' x)
then show ?case
proof(induct x)
case (TEEC_INITIALIZECONTEXT x1 x2a)
then show ?case
proof -
let ?e = "hyperc' (TEEC_INITIALIZECONTEXT x1 x2a)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_InitializeContextR sysconf s x1 x2a))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_InitializeContext sysconf (⇑s) x1 x2a))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_INITIALIZECONTEXT TEEC_InitializeContextR_refine a1
by metis
qed
next
case (TEEC_FINALIZECONTEXT x1)
then show ?case
using TEEC_FINALIZECONTEXT TEEC_FinalizeContextR_refine
exec_eventR_def exec_event_def eR_def by simp
next
case (TEEC_OPENSESSION1 x1 x2a x3 x4 x5a x6 x7)
then show ?case
proof -
let ?e = "hyperc' (TEEC_OPENSESSION1 x1 x2a x3 x4 x5a x6 x7)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst((TEEC_OpenSession1R sysconf s x1 x2a x3 x4 x5a x6 x7)))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_OpenSession1 sysconf (⇑s) x1 x2a x3 x4 x5a x6 x7))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_OPENSESSION1 TEEC_OpenSession1R_refine a1
by metis
qed
next
case TEEC_OPENSESSION2
then show ?case
proof -
let ?e = "hyperc' TEEC_OPENSESSION2"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_OpenSession2R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_OpenSession2 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_OPENSESSION2 TEEC_OpenSession2R_refine a1
by metis
qed
next
case (TEEC_OPENSESSION3 x)
then show ?case
proof -
let ?e = "hyperc' (TEEC_OPENSESSION3 x)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_OpenSession3R sysconf s x))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_OpenSession3 sysconf (⇑s) x))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_OPENSESSION3 TEEC_OpenSession3R_refine a1
by metis
qed
next
case TEEC_OPENSESSION4
then show ?case
proof -
let ?e = "hyperc' TEEC_OPENSESSION4"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_OpenSession4R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_OpenSession4 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_OPENSESSION4 TEEC_OpenSession4R_refine a1
by metis
qed
next
case (TEEC_CLOSESESSION1 x1 x2a x3 x4)
then show ?case
proof -
let ?e = "hyperc' (TEEC_CLOSESESSION1 x1 x2a x3 x4)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_CloseSession1R sysconf s x1 x2a x3 x4))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_CloseSession1 sysconf (⇑s) x1 x2a x3 x4))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_CLOSESESSION1 TEEC_CloseSession1R_refine a1
by metis
qed
next
case TEEC_CLOSESESSION2
then show ?case
proof -
let ?e = "hyperc' TEEC_CLOSESESSION2"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_CloseSession2R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_CloseSession2 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_CLOSESESSION2 TEEC_CloseSession2R_refine a1
by metis
qed
next
case TEEC_CLOSESESSION3
then show ?case
proof -
let ?e = "hyperc' TEEC_CLOSESESSION3"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_CloseSession3R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_CloseSession3 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_CLOSESESSION3 TEEC_CloseSession3R_refine a1
by metis
qed
next
case TEEC_CLOSESESSION4
then show ?case
proof -
let ?e = "hyperc' TEEC_CLOSESESSION4"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_CloseSession4R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_CloseSession4 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_CLOSESESSION4 TEEC_CloseSession4R_refine a1
by metis
qed
next
case (TEEC_INVOKECOMMAND1 x1 x2a x3 x4 x5a x6)
then show ?case
proof -
let ?e = "hyperc' (TEEC_INVOKECOMMAND1 x1 x2a x3 x4 x5a x6)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_InvokeCommand1R sysconf s x1 x2a x3 x4 x5a x6))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_InvokeCommand1 sysconf (⇑s) x1 x2a x3 x4 x5a x6))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_INVOKECOMMAND1 TEEC_InvokeCommand1R_refine a1
by metis
qed
next
case TEEC_INVOKECOMMAND2
then show ?case
proof -
let ?e = "hyperc' (TEEC_INVOKECOMMAND2)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_InvokeCommand2R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_InvokeCommand2 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_INVOKECOMMAND2 TEEC_InvokeCommand2R_refine a1
by metis
qed
next
case TEEC_INVOKECOMMAND3
then show ?case
proof -
let ?e = "hyperc' (TEEC_INVOKECOMMAND3)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_InvokeCommand3R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_InvokeCommand3 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_INVOKECOMMAND3 TEEC_InvokeCommand3R_refine a1
by metis
qed
next
case TEEC_INVOKECOMMAND4
then show ?case
proof -
let ?e = "hyperc' (TEEC_INVOKECOMMAND4)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_InvokeCommand4R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_InvokeCommand4 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_INVOKECOMMAND4 TEEC_InvokeCommand4R_refine a1
by metis
qed
next
case (TEEC_REGISTERSHAREDMEMORY x1 x2a)
then show ?case
proof -
let ?e = "hyperc' (TEEC_REGISTERSHAREDMEMORY x1 x2a)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_RegisterSharedMemoryR sysconf s x1 x2a))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_RegisterSharedMemory sysconf (⇑s) x1 x2a))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_REGISTERSHAREDMEMORY TEEC_RegisterSharedMemoryR_refine a1
by metis
qed
next
case (TEEC_ALLOCATESHAREDMEMORY x1 x2a)
then show ?case
proof -
let ?e = "hyperc' (TEEC_ALLOCATESHAREDMEMORY x1 x2a)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEEC_AllocateSharedMemoryR sysconf s x1 x2a))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEEC_AllocateSharedMemory sysconf (⇑s) x1 x2a))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_ALLOCATESHAREDMEMORY TEEC_AllocateSharedMemoryR_refine a1
by metis
qed
next
case (TEEC_RELEASESHAREDMEMORY x)
then show ?case
proof -
let ?e = "hyperc' (TEEC_RELEASESHAREDMEMORY x)"
have a1:"(s,t)∈exec_eventR ?e = (t=(TEEC_ReleaseSharedMemoryR sysconf s x))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=(TEEC_ReleaseSharedMemory sysconf (⇑s) x))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEEC_RELEASESHAREDMEMORY TEEC_ReleaseSharedMemoryR_refine a1
by metis
qed
next
case TEE_OPENTASESSION1
then show ?case
proof -
let ?e = "hyperc' (TEE_OPENTASESSION1)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst((TEE_OpenTASession1R sysconf s)))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_OpenTASession1 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_OPENTASESSION1 TEE_OpenTASession1R_refine a1
by metis
qed
next
case TEE_OPENTASESSION2
then show ?case
proof -
let ?e = "hyperc' (TEE_OPENTASESSION2)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst((TEE_OpenTASession2R sysconf s)))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_OpenTASession2 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_OPENTASESSION2 TEE_OpenTASession2R_refine a1
by metis
qed
next
case (TEE_OPENTASESSION3 x)
then show ?case
proof -
let ?e = "hyperc' (TEE_OPENTASESSION3 x)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst((TEE_OpenTASession3R sysconf s x)))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_OpenTASession3 sysconf (⇑s) x))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_OPENTASESSION3 TEE_OpenTASession3R_refine a1
by metis
qed
next
case TEE_OPENTASESSION4
then show ?case
proof -
let ?e = "hyperc' (TEE_OPENTASESSION4)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst((TEE_OpenTASession4R sysconf s)))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_OpenTASession4 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_OPENTASESSION4 TEE_OpenTASession4R_refine a1
by metis
qed
next
case (TEE_INVOKETACOMMAND1 x)
then show ?case
proof -
let ?e = "hyperc' (TEE_INVOKETACOMMAND1 x)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_InvokeTACommand1R sysconf s x))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_InvokeTACommand1 sysconf (⇑s) x))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_INVOKETACOMMAND1 TEE_InvokeTACommand1R_refine a1
by metis
qed
next
case TEE_INVOKETACOMMAND2
then show ?case
proof -
let ?e = "hyperc' (TEE_INVOKETACOMMAND2)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_InvokeTACommand2R sysconf s ))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_InvokeTACommand2 sysconf (⇑s) ))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_INVOKETACOMMAND2 TEE_InvokeTACommand2R_refine a1
by metis
qed
next
case TEE_INVOKETACOMMAND3
then show ?case
proof -
let ?e = "hyperc' (TEE_INVOKETACOMMAND3)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_InvokeTACommand3R sysconf s ))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_InvokeTACommand3 sysconf (⇑s) ))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_INVOKETACOMMAND3 TEE_InvokeTACommand3R_refine a1
by metis
qed
next
case TEE_INVOKETACOMMAND4
then show ?case
proof -
let ?e = "hyperc' (TEE_INVOKETACOMMAND4)"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_InvokeTACommand4R sysconf s ))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_InvokeTACommand4 sysconf (⇑s) ))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_INVOKETACOMMAND4 TEE_InvokeTACommand4R_refine a1
by metis
qed
next
case TEE_CLOSETASESSION1
then show ?case
proof -
let ?e = "hyperc' TEE_CLOSETASESSION1"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_CloseTASession1R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_CloseTASession1 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_CLOSETASESSION1 TEE_CloseTASession1R_refine a1
by metis
qed
next
case TEE_CLOSETASESSION2
then show ?case
proof -
let ?e = "hyperc' TEE_CLOSETASESSION2"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_CloseTASession2R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_CloseTASession2 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_CLOSETASESSION2 TEE_CloseTASession2R_refine a1
by metis
qed
next
case TEE_CLOSETASESSION3
then show ?case
proof -
let ?e = "hyperc' TEE_CLOSETASESSION3"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_CloseTASession3R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_CloseTASession3 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_CLOSETASESSION3 TEE_CloseTASession3R_refine a1
by metis
qed
next
case TEE_CLOSETASESSION4
then show ?case
proof -
let ?e = "hyperc' TEE_CLOSETASESSION4"
have a1:"(s,t)∈exec_eventR ?e = (t=fst(TEE_CloseTASession4R sysconf s))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=fst(TEE_CloseTASession4 sysconf (⇑s)))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_CLOSETASESSION4 TEE_CloseTASession4R_refine a1
by metis
qed
next
case (TEE_CHECKMEMORYACCESSRIGHTS x1 x2a x3)
then show ?case
proof -
let ?e = "hyperc' (TEE_CHECKMEMORYACCESSRIGHTS x1 x2a x3)"
have a1:"(s,t)∈exec_eventR ?e = (t=s)"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=(⇑s))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_CHECKMEMORYACCESSRIGHTS a1
by metis
qed
next
case (TEE_MALLOC x1 x2a)
then show ?case
proof -
let ?e = "hyperc' (TEE_MALLOC x1 x2a)"
have a1:"(s,t)∈exec_eventR ?e = (t=(TEE_MallocR sysconf s x1 x2a))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=(TEE_Malloc sysconf (⇑s) x1 x2a))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_MALLOC TEE_MallocR_refine a1
by metis
qed
next
case (TEE_REALLOC x1 x2a)
then show ?case
proof -
let ?e = "hyperc' (TEE_REALLOC x1 x2a)"
have a1:"(s,t)∈exec_eventR ?e = (t=(TEE_ReallocR sysconf s x1 x2a))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=(TEE_Realloc sysconf (⇑s) x1 x2a))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_REALLOC TEE_ReallocR_refine a1
by metis
qed
next
case (TEE_FREE x)
then show ?case
proof -
let ?e = "hyperc' (TEE_FREE x)"
have a1:"(s,t)∈exec_eventR ?e = (t=(TEE_FreeR sysconf s x))"
using exec_eventR_def by auto
have a2:"(⇑s,⇑t)∈exec_event ((eR ?e)) = ((⇑t)=(TEE_Free sysconf (⇑s) x))"
using exec_event_def eR_def abstract_state_def by simp
then show ?thesis
using TEE_FREE TEE_FreeR_refine a1
by metis
qed
qed
next
case (sys' x)
then show ?case using sysR_refine
by (metis (mono_tags, lifting) SyscallR.exhaust)
qed
qed
lemma reachR_reach1:
"∀s as s'. GPTEE_Instantiation.reachable0 (⇑s) ∧
reachable0 s ∧ s'∈execute as s ⟶
GPTEE_Instantiation.reachable0 (⇑s')"
proof -
{
fix as
have "∀s s'. GPTEE_Instantiation.reachable0 (⇑s) ∧
reachable0 s ∧ s'∈execute as s ⟶ GPTEE_Instantiation.reachable0 (⇑s')"
proof(induct as)
case Nil
then show ?case using reachable0_def execute_def by auto
next
case (Cons a as)
assume a0:"∀s s'. GPTEE_Instantiation.reachable0 (⇑s) ∧
reachable0 s ∧ s'∈execute as s ⟶ GPTEE_Instantiation.reachable0 (⇑s')"
show ?case
proof -
{
fix s s'
assume b0:"GPTEE_Instantiation.reachable0 (⇑s) ∧
reachable0 s ∧ s'∈execute (a#as) s"
have b3: "∀s1. (s,s1)∈exec_eventR a ⟶ GPTEE_Instantiation.reachable0 (⇑s1)"
proof -
{
fix s1
assume c0: "(s,s1)∈exec_eventR a"
then have "GPTEE_Instantiation.reachable0 (⇑s1)"
using GPTEE_Instantiation.reachableStep b0 refine_exec_event by metis
}
then show ?thesis by auto
qed
from b0 have "∃s1. (s,s1)∈exec_eventR a ∧ (s1,s')∈run as" using reachable0_def execute_def by auto
then obtain s1 where b4:"(s,s1)∈exec_eventR a ∧ (s1,s')∈run as" by auto
have b5:"GPTEE_Instantiation.reachable0 (⇑s1)" using b3 b4 by auto
have b6:"Design_Instantiation.reachable0 s1" using reachableStep b0 b4 by blast
have "GPTEE_Instantiation.reachable0 (⇑s')" using b4 b5 a0 b6 execute_def by auto
}
then show ?thesis by auto
qed
qed
} then show ?thesis by auto
qed
lemma reachR_reach: "reachable0 s ⟹ GPTEE_Instantiation.reachable0 (⇑s)"
using reachR_reach1 Design_Instantiation.reachable0_def reachable_s0
GPTEE_Instantiation.reachable_s0 s0_ref_lemma execute_def reachable_def
by (metis Image_singleton_iff)
lemma weak_confidentiality_evt_ref:
"∀e. GPTEE_Instantiation.weak_confidentiality_e ((eR e))
∧ weak_confidentiality_new_e e ⟶ Design_Instantiation.weak_confidentiality_e e"
using GPTEE_Instantiation.weak_confidentiality_e_def Design_Instantiation.weak_confidentiality_e_def
domain_domainR reachR_reach refine_exec_event
vpeqR_def vpeqR_vpeq1 weak_confidentiality_new_e_def abstract_state_def
by (smt (verit, ccfv_threshold) State.select_convs(2) State.select_convs(4)
State.select_convs(6) get_exec_primeR_def get_exec_prime_def)
lemma integrity_evt_ref:
"∀e. GPTEE_Instantiation.integrity_e ((eR e))
∧ integrity_new_e e ⟶ Design_Instantiation.integrity_e e"
using Design_Instantiation.integrity_e_def GPTEE_Instantiation.integrity_e_def
GPTEE_Instantiation.non_interference_def domain_domainR integrity_new_e_def
non_interference1_def reachR_reach refine_exec_event vpeqR_def by metis
lemma abs_sc_new_imp: "⟦GPTEE_Instantiation.weak_confidentiality; weak_confidentiality_new⟧
⟹ Design_Instantiation.weak_confidentiality"
using Design_Instantiation.weak_confidentiality_all_evt GPTEE_Instantiation.weak_confidentiality_all_evt
weak_confidentiality_evt_ref weak_confidentiality_new_all_evt
by blast
lemma abs_lr_new_imp: "⟦GPTEE_Instantiation.integrity; integrity_new⟧ ⟹ Design_Instantiation.integrity"
using Design_Instantiation.integrity_all_evt GPTEE_Instantiation.integrity_all_evt
integrity_evt_ref integrity_new_all_evt by blast
section "Design layer Security"
subsection "syscall aux lemma"
lemma syscallR_integrity:
assumes p1: "a = sys' Reserved"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_eventR s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_eventR a"
have "s'=s" using exec_eventR_def a3 p1 by simp
then have "s∼. d .∼Δ s'" by auto
}
then show ?thesis by blast
qed
lemma syscallR_integrity_e:
"integrity_new_e (sys' Reserved)"
using syscallR_integrity integrity_new_e_def
by auto
lemma syscallR_weak_confidentiality:
assumes p1: "a = sys' Reserved"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼. d .∼ t) ∧
((domain_of_eventR s a) = (domain_of_eventR t a)) ∧
(get_exec_primeR s=get_exec_primeR t)∧
((the (domain_of_eventR s a)) ↝ d) ∧
(s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼.d.∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)"
assume a5:"(the (domain_of_eventR s a)) ↝ d"
assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t"
assume a7:"(s, s') ∈ exec_eventR a"
assume a8:"(t, t') ∈ exec_eventR a"
have b1:"s'=s" using a7 p1 exec_eventR_def by auto
have b2:"t'=t" using a8 p1 exec_eventR_def by auto
then have "(s' ∼. d .∼Δ t')" using b1 b2 a3 by simp
}
then show ?thesis using get_exec_primeR_def
by (smt (verit, ccfv_SIG) Pair_inject)
qed
lemma syscallR_weak_confidentiality_e:
"weak_confidentiality_new_e (sys' Reserved)"
using syscallR_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def
by (smt (verit, del_insts) Pair_inject)
subsection "design layer new variable security"
theorem weak_confidentiality_new:weak_confidentiality_new
proof -
{
fix e
have "weak_confidentiality_new_e e"
proof(induct e)
case (hyperc' x)
show ?case
using TEEC_InitializeContextR_weak_confidentiality_e TEEC_FinalizeContextR_weak_confidentiality_e
TEEC_OpenSession1R_weak_confidentiality_e TEEC_OpenSession2R_weak_confidentiality_e
TEEC_OpenSession3R_weak_confidentiality_e TEEC_OpenSession4R_weak_confidentiality_e TEEC_CloseSession1R_weak_confidentiality_e
TEEC_CloseSession2R_weak_confidentiality_e TEEC_CloseSession3R_weak_confidentiality_e TEEC_CloseSession4R_weak_confidentiality_e
TEEC_InvokeCommand1R_weak_confidentiality_e TEEC_InvokeCommand2R_weak_confidentiality_e
TEEC_InvokeCommand3R_weak_confidentiality_e TEEC_InvokeCommand4R_weak_confidentiality_e TEEC_RegisterSharedMemoryR_weak_confidentiality_e
TEEC_AllocateSharedMemoryR_weak_confidentiality_e
TEEC_ReleaseSharedMemoryR_weak_confidentiality_e TEE_OpenTASession1R_weak_confidentiality_e
TEE_OpenTASession2R_weak_confidentiality_e TEE_OpenTASession3R_weak_confidentiality_e TEE_OpenTASession4R_weak_confidentiality_e
TEE_InvokeTACommand1R_weak_confidentiality_e TEE_InvokeTACommand2R_weak_confidentiality_e
TEE_InvokeTACommand3R_weak_confidentiality_e TEE_InvokeTACommand4R_weak_confidentiality_e TEE_CloseTASession1R_weak_confidentiality_e
TEE_CloseTASession2R_weak_confidentiality_e TEE_CloseTASession3R_weak_confidentiality_e TEE_CloseTASession4R_weak_confidentiality_e
TEE_CheckMemoryAccessRightsR_weak_confidentiality_e
TEE_MallocR_weak_confidentiality_e TEE_ReallocR_weak_confidentiality_e
TEE_FreeR_weak_confidentiality_e apply (rule HypercallR.induct) done
next
case (sys' x)
show ?case using syscallR_weak_confidentiality_e SyscallR.induct
by fastforce
qed
}
then show ?thesis
by (simp add: weak_confidentiality_new_all_evt)
qed
theorem integrity_new:integrity_new
proof -
{
fix e
have "integrity_new_e e"
proof(induct e)
case (hyperc' x)
show ?case
using TEEC_InitializeContextR_integrity_e TEEC_FinalizeContextR_integrity_e
TEEC_OpenSession1R_integrity_e TEEC_OpenSession2R_integrity_e
TEEC_OpenSession3R_integrity_e TEEC_OpenSession4R_integrity_e TEEC_CloseSession1R_integrity_e
TEEC_CloseSession2R_integrity_e TEEC_CloseSession3R_integrity_e TEEC_CloseSession4R_integrity_e
TEEC_InvokeCommand1R_integrity_e TEEC_InvokeCommand2R_integrity_e
TEEC_InvokeCommand3R_integrity_e TEEC_InvokeCommand4R_integrity_e TEEC_RegisterSharedMemoryR_integrity_e
TEEC_AllocateSharedMemoryR_integrity_e
TEEC_ReleaseSharedMemoryR_integrity_e TEE_OpenTASession1R_integrity_e
TEE_OpenTASession2R_integrity_e TEE_OpenTASession3R_integrity_e TEE_OpenTASession4R_integrity_e
TEE_InvokeTACommand1R_integrity_e TEE_InvokeTACommand2R_integrity_e
TEE_InvokeTACommand3R_integrity_e TEE_InvokeTACommand4R_integrity_e TEE_CloseTASession1R_integrity_e
TEE_CloseTASession2R_integrity_e TEE_CloseTASession3R_integrity_e TEE_CloseTASession4R_integrity_e
TEE_CheckMemoryAccessRightsR_integrity_e
TEE_MallocR_integrity_e TEE_ReallocR_integrity_e
TEE_FreeR_integrity_e apply (rule HypercallR.induct) done
next
case (sys' x)
show ?case using syscallR_integrity_e SyscallR.induct
by fastforce
qed
}
then show ?thesis
by (simp add: integrity_new_all_evt)
qed
theorem des_weak_confidentiality: weak_confidentiality
using req_weak_confidentiality weak_confidentiality_new abs_sc_new_imp by blast
theorem des_integrity: integrity
using req_integrity integrity_new abs_lr_new_imp by blast
theorem des_confidentiality: confidentiality
using des_weak_confidentiality des_integrity weak_with_step_cons
by blast
end